Automated, Credible Autocoding of An Unmanned Aggressive Maneuvering Car Controller

摘要

This article describes the application of a credible autocoding framework forcontrol systems towards a nonlinear car controller example. The frameworkgenerates code, along with guarantees of high level functional properties aboutthe code that can be independently verified. These high-level functionalproperties not only serves as a certificate of good system behvaior but alsocan be used to guarantee the absence of runtime errors. In one of our previousworks, we have constructed a prototype autocoder with proofs that demonstratesthis framework in a fully automatic fashion for linear and quasi-nonlinearcontrollers. With the nonlinear car example, we propose to further extend theprototype's dataflow annotation language environment with with several newannotation symbols to enable the expression of general predicates and dynamicalsystems. We demonstrate manually how the new extensions to the prototypeautocoder work on the car controller using the output language Matlab. Finally,we discuss the requirements and scalability issues of the automatic analysisand verification of the documented output code.